perm filename W77.OUT[LET,JMC] blob sn#274158 filedate 1977-04-05 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	∂14-Mar-77  1353	JMC  
C00034 ENDMK
C⊗;
∂14-Mar-77  1353	JMC  
To:   RWW    
I think the FOL jproject should be described in a way that shows
change.  Why don't you try to put it into the following format.

	The FOL proof-checker is now able to check almost all
the kinds of reasoning for which it was designed.
Weyhrauch (1977) is a collection of these proofs.  As expected, they
are longer than human informal proofs, but they are about the
first machine-checked complete proofs of substantial results
in mathematics, program correctness, and the theory of knowledge.

	We are now
entering a new phase of the work.  The next step is to reduce
the size of the human contribution to the reasoning by introducing
shortcuts.  A large group of shorcuts has been programmed and
are ready to be tested on substantial problems.  These included

	a.
	b.



	During the next year and a half, we plan the following
proofs:

∂14-Mar-77  1338	JMC  
To:   ZM
Please look at mtc.pro[w77,jmc].  No protection.

∂14-Mar-77  1222	JMC  
To:   carl at MIT-AI   
You may be interested in EXOTIC[W77,JMC].  I would welcome your comments.

∂14-Mar-77  1154	JMC  
To:   MJL    
Tomorrow at 4:00 is ok.  Please confirm.

∂14-Mar-77  0944	JMC  
To:   JAB    
Your suggestion seems fine.  Yes, you may audit.

∂13-Mar-77  1745	JMC  	Your writeup. 
To:   CG
Yours is too technical for ARPA.  It would need a Scientific American
level summary.  Also it is somewhat remote from application - even
for me.  However, it isn't essential that you have one.  Naturally,
I would hope you would do something more on non-knowledge also.

∂12-Mar-77  2354	JMC  
To:   ME
;:;oooogggggggggggggggooooooooooggggggggggggg99ll

∂12-Mar-77  1525	JMC  
To:   * 
Can anyone give a reference to a mathematical treatment of Instant Insanity? - JMC

∂12-Mar-77  1506	JMC  	Colloquium    
To:   MJL    
Please tell whoever is in charge of the colloquium
(Is it still Frances Yao?) that I would like to
give one entitled "Representing Recursive Programs in First
Order Logic".

∂12-Mar-77  1056	JMC  
To:   rsmith at RUTGERS-10  
Just checking if mail to rutg works.

∂12-Mar-77  1055	JMC  
To:   smith at RUTGERS-10   
Just checking if mail to rutg works.

∂12-Mar-77  1055	JMC  
To:   rs at RUTGERS-10 
Just checking if mail to rutg works.

∂12-Mar-77  1050	JMC  
To:   joseph at MIT-MC 
I haven't drawn a precise line in my mind, and it isn't necessary to
have a precise line in  order to decide some cases.  Certainly I would
say that anyone not charged with a crime is entitled to leave any
country including his own.  This is what the U.N. Declaration on human
rights says.  If there were an absolute right to depart, one country
might give sanctuary to another's criminals as a means of encouraging
crime in that country, but I doubt many would find it worthwhile.
Castro found the hijackers a pain in the neck, and I wonder it the
North Koreans, who, I seem to remember, offered to take the Attica
rebel prisoners, would have been happy with them.  An absolute agreement
to let anyone out wouldn't be bad.  We wouldn't even lose too much
if we unilaterally let all spies go except those, if any, who had
just stolen a vital secret (if any) and hadn't been able to transmit
it.

∂12-Mar-77  0204	JMC  
To:   MJC    
I was here first

∂10-Mar-77  1636	JMC  	Conjecture fails.  
To:   MFB, ND
tau[f](x) = if f h1 x = omega ∧ f h2 x = omega then omega else 1

is continuous but not of the usual form, i.e. it can't be written
without explicit mention of omega, and it can't be computed except
by computing f h1 x and f h2 x in parallel so that whichever returns
causes tau[f](x) to have value 1.

∂10-Mar-77  1624	JMC  	Not really a new case.  
To:   MFB    
We have not mentioned, but have always had the case

	tau[f](x) = m1(x,f h x).

Its least fixed point  is the totally undefined function.  But

	if m f h x then g1 x else g2 x = m1(x,f h x)

where

	m1(x,y) = if m y then g1 x else g2 x.

∂10-Mar-77  1054	JMC  
To:   feigenbaum at SUMEX-AIM    
I hope the title of "Professor of Combinatorics" for Chvatal remains,
because this was an essential factor in my positive vote in allowing
me to hope that the appointment wouldn't unduly mortgage the chances
of getting new people in C.S., especially AI.

∂10-Mar-77  1050	JMC  
To:   bobrow at PARC-MAXC   
I am glad to accept your invitation, and the deadline offers no problem.

∂09-Mar-77  1759	JMC  
To:   PAT    
Please fill out the form on Gumb's proposal using nsf.re2[let,jmc].

∂09-Mar-77  1603	JMC  
To:   MJL    
How much does one have to drink for the AA Qual?

∂08-Mar-77  2207	JMC  
To:   ME, LES
I am not much impressed with the cost-effectiveness of the latest E mods.

∂08-Mar-77  1549	JMC  	Guy Steele visit   
To:   gls at MIT-AI
CC:   RWG, LES   
We will be glad to have you in July in accordance with the suggestions
in your message to Knuth and Gosper, and we can help with expenses.

∂07-Mar-77  1423	JMC  
To:   dbrown at SUMEX-AIM, feigenbaum at SUMEX-AIM   
Oral announcement.

∂07-Mar-77  1151	JMC  
To:   feigenbaum at SUMEX-AIM, dbrown at SUMEX-AIM   
AI Lab policy on CSD use

	1. We hereby offer accounts to all CSD faculty.  Message use and
document preparation are solicited.  If use by typists is wanted, this
can be negotiated.  Arrange accounts with Lester Earnest at the Lab.
The Lab can't provide terminals, but we recommend Datamedias in the
configuration that our editor supports.
Faculty members should state whether they plan to log in
often enough so that messages are reliably received.

	2. PhD students who request accounts will receive them with
probability near one.  Preparation of theses is tentatively welcome.
We reserve the right to get stingy if we are overwhelmed, but we don't
expect it.

	3. Use properly belonging on other machines is not welcomed.
Thus students with RAs on projects using SUMEX or IMSSS are expected to use
those computers, and students taking courses that use LOTS are expected
to do the course work on LOTS.

	4. No-one should log in on the AI Lab computer remotely and
then go out on the ARPA net or dial-out lines.  These programs
use up memory space and computer time out of proportion to what they
accomplish.  Remote computers should be used directly.

	5. We don't want to post this policy.  Stanford owns the KL-10
received as a gift from D.E.C. and other equipment given us by the
government.  The government owns some of the equipment and pays for
maintenance.  Figuring out the exact fraction of the computer we can
thereby dispose of for non-government purposes would be complicated
and subjective and is better put off until it becomes necessary for
other reasons.

∂07-Mar-77  0110	JMC  
To:   LES    
If you agree, I'll send POLICY[W77,JMC] to Feigenbaum and D. Brown.

∂06-Mar-77  1351	JMC  
CC:   dbrown at SUMEX-AIM   
les,feigenbaum%sumex

∂06-Mar-77  1342	JMC  	Your request. 
To:   TOG    
I have inquired, and no-one has a project for which they
consider you suitable.  Furthermore, you ran up a big Pony
bill and haven't paid it.  Please don't use this computer
any more.

∂05-Mar-77  1212	JMC  
To:   pratt at MIT-AI  
No, I haven't been thinking about CGOL though I may get back to it.

∂05-Mar-77  1211	JMC  
CC:   JBR, LES, PMF    
 ∂05-Mar-77  0232	TOG  	ACCOUNTS 
JOHN, IS THERE A PROJECT THAT COULD USE SOME HELP,I WOULD LIKE TO USE THE
FACILITY?                     TODD GLASSEY

∂02-Mar-77  2335	JMC  
To:   DEK    
Thanks for the loan of the tiles.

∂02-Mar-77  2215	JMC  
To:   MFB    
Since you may have to refer to it, remember it's spelled Vuillemin.

∂02-Mar-77  1616	JMC  	MI9 
To:   phw at MIT-AI, buchanan at SUMEX-AIM 
The attendance, including the Soviet attendance, at MI9 looks interesting
enough so that I have decided to go.

∂02-Mar-77  1143	JMC  
To:   HVA    
I don't remember any such thing, but you'd better check such matters
directly.  I try to turn over such communications to you or Les.

∂02-Mar-77  1057	JMC  
To:   AIQUAL.LST[W77,JMC]:; 
I have asked Moira to post a notice asking who intends to take the
qual.  We can then decide on format.

∂01-Mar-77  2247	JMC  	Movie Projector    
To:   LES    
If, as seems likely, our projector has been stolen again, I
suggest the next one be chained and bolted to a wheeled table.

∂01-Mar-77  1803	JMC  
To:   TED    
The terminal in Martin Davis's office squeals like a dying bat.

∂28-Feb-77  2108	JMC  
To:   ALS, ME
The page on Imlacs in the E manual is outdated and should be deleted.

∂27-Feb-77  2216	JMC  
To:   minsky at MIT-AI 
Thanks, I'll transmit content to Suppes.

∂27-Feb-77  2100	JMC  
To:   JAB    
Yes, it would.

∂25-Feb-77  1851	JMC  
To:   PAT    
DIALNE.LST contains some notes on who should get Dialnet memos.
Please ask me for help in making it into a proper list.

∂25-Feb-77  0958	JMC  
To:   JAB    
It would be important for both LOTS and SRI to maintain compatibility
with M.I.T.

∂23-Feb-77  2346	JMC  
To:   DSB    
There is no prospect of replacing the ADM3s for two years.

∂23-Feb-77  1320	JMC  
CC:   PMF, RPG    
 ∂23-Feb-77  1312	FTP:Dang at SRI-AI	Maclisp for Tops-20  
Date: 22 Feb 1977 2318-PST
From: Dang at SRI-AI
Subject: Maclisp for Tops-20
To:   JCM at SAIL
cc:   JAB at SAIL, DanG

Hello.  John Borchek was telling me that you wanted to have a copy of
Maclisp on Lots, possibly to be used in a lisp course at Stanford.
Right now I am in the middle of trying to make Maclisp run a little
better under Tops-20, but I can give you the origional Tops-10 version
of Maclisp 1251 running with the DEC PA1050 compatibility package.

So far it appears to be working just fine, but since nobody is supporting
Maclisp for Tops-20 except for the limited amount of work that I have
been doing, I would really appreciate it if you could forward all comments, 
bugs, and fixes to me and I will look into fixing it for our users here 
at SRI too.  I will also add your name, as well as anyone else you like,
to the Maclisp distribution list that I am preparing so that you will 
get the information on newer versions of Maclisp as they are created.

On the tape that I am will drop by tomorrow,  I am adding the compiler
(Ncomplr), Grindef, Pratt's CGOL, as well as other assorted library
routines that might be useful.  I will send over another tape at a
later date containing more library routines from MIT-MC as I tranport
them.  Most of this has not been tested much either, if at all, so
again, use them with care.

If there is any way at all that I can assist you, please feel free
to send me a message.

Dan Gerson
-------

∂23-Feb-77  0930	JMC   via USCT 
To:   LES    
Received somewhat soothing message from Russell.

∂23-Feb-77  0925	JMC   via USCT 
To:   russell at USC-ISI    
Sorry mixed my message to you with Ed's message to me.

∂23-Feb-77  0907	JMC  
To:   russell at USC-ISI    
 ∂23-Feb-77  0313	FTP:Feigenbaum at SUMEX-AIM	march 4 meeting at arpa    
Date: 22 FEB 1977 1817-PST
From: Feigenbaum at SUMEX-AIM
Subject: march 4 meeting at arpa
To:   les at SU-AI, jmc at SU-AI

The meeting on March 4 is in the MORNING, not afternoon as
previously mentioned. Participants from Stanford are jmc,les,and eaf.
Particiaants on their side are col. russell and I don't know who else.

ed
-------

I understsand your position better now.  We have nsf visit
Thurs and Fri at which I can raise question of thix their
support of basic AI work aaxx at Stanford.  I will try
to phone you on Monday.

∂22-Feb-77  0207	JMC  
To:   PAT    
Please xs sato.xgp[w77,jmc] and sato.xgp[let,jmc].  I'll be back Thurs.

∂21-Feb-77  0110	JMC  
To:   ZM
What is the reference on subgoal induction?

∂20-Feb-77  2205	JMC  
To:   PMF    
I have put part3.xgp in [206,lsp] which is where it should be.

∂20-Feb-77  1629	JMC  
To:   WHG    
I take it back.  I now think call-by-value is right.

∂19-Feb-77  1407	JMC  
To:   RSC    
FIRST and FIRST.NEW on [W77,JMC] may interest.  They are evolving.

∂19-Feb-77  1000	JMC  	Dirt and mess 
To:   LES, HVA    
How can we get the machine room and other places cleaned up?
I suspect they make a bad impression on funders.

∂18-Feb-77  1337	JMC  	Theoretical work in AI  
To:   russell at USC-ISI    
Is it correct than ARPA is no longer willing to support
theoretical work in AI?  There is already too little theoretical
work as it is, and I would like the opportunity to argue this
point.

∂18-Feb-77  1119	JMC  
To:   JBR    
How is a load average of .8 compatible with a disk queue of 18?

∂18-Feb-77  1000	JMC  	dialer   
To:   TED    
The dialer isn't working again.  When it dials a number, it lets it ring
once and then reports a time-out error.  Perhaps the timer is just set
too short.

∂17-Feb-77  2044	JMC  	Machine Intelligence Workshop
To:   phw at MIT-AI    
Do you remember who else Michie said was going from this country.  We could
tell Michie to tell the Russians that attendance would be great if
Lerner received an exit visa.

∂17-Feb-77  1624	JMC  
To:   * 
5505 is reserved for a demo from 8:30 to 10:30 tonight Thursday

∂16-Feb-77  2150	JMC  
To:   DCL    
It appeared in a book edited by Tom Steele with a title like
"Formal language definition languages".  Maybe I can find it, and since
I don't recall it as a popular paper, there may still be reprints.

∂16-Feb-77  1459	JMC  	Non-autologut.
To:   EJG    
As long as I am so subject to interruption, I need to keep the privilege.
I have no objection to your suggestion, but elaboration of the privilege
structure is very low priority.

∂16-Feb-77  1458	JMC  
To:   RS
Many thanks for Ulam's book which I have just read.

∂14-Feb-77  2152	JMC  
To:   BPM    
Well, if someone were to rewrite Telnet for greater efficiency, ...

∂14-Feb-77  2103	JMC  	IMSSS and TELNET   
To:   BPM, TOB    
These programs are quite expensive to use.  Communication with other
computers from remote terminals should be done directly or through the
TIP whenever possible.  BPM was just taking 26% PL.

∂14-Feb-77  1407	JMC  
To:   RWW    
It will have the extension .prf if it still exists.

∂12-Feb-77  1625	JMC  
To:   DCL    
What are the other reasons?

∂11-Feb-77  2343	JMC  
To:   PMF    
It would be good to get some Lisp on LOTS quite soon.

∂11-Feb-77  1810	JMC  	A Natural Representation
To:   ND, WP 
The result came out better than I expected.  I have put notes in your
boxes, but you can also read REPRES[W77,JMC] if you don't mind the PUB.

∂11-Feb-77  1526	JMC  	Jarvis board  
To:   PMF    
John Gill, ESL, is interested in getting one or two for the PDP-11
they are expecting in May.  You might call him about the present
state of the redesign.

∂11-Feb-77  1503	JMC  
To:   * 
USGS earthquake predictors can hire student to work on data handling.
Call Chuck Bufe, 323-8111 x2568

∂11-Feb-77  1011	JMC  	DIAL
To:   JBR    
Erik Gilbert was using DIAL last night at 10 chars/sec and achieved
a PL of 14%.  If the KL does an instruction per microsecond, this
represents 14,000 instruction executions per character transferred.
How can this be?

∂11-Feb-77  0132	JMC  
To:   ND
If I understand your formula correctly, then the recursive definition

	f x ← if p x then x else f h x

gives rise to the sentence

∀x.(y = f x ≡ ∃w.[x.y ε w ∧ ∀u v.[u.v ε w ⊃ ∀z.[(h u . z) ε w ∧
			v = if p u then u else z]]]).

This doesn't seem right.  It looks like ∀z should read ∃z, but
even then the terminating case isn't handled right.  I think we
want

∀x.(y = f x ≡ ∃w.[x.y ε w ∧ ∀u v.[u.v ε w ⊃ 
	if p u then v = u else ∃z.[(h u . z) ε w].

No, this doesn't work either, because the recursive definition
f x ← f x
would let us conclude that f x = 196.

∂10-Feb-77  2023	JMC  
To:   RPG    
I have FTPed the file to PART3[W77,JMC], but it doesn't seem to be
lineprinter PUB output.  What do you make of it?

 ∂10-Feb-77  1916	FTP:ELLEN at MIT-MC (V. Ellen Lewis )   
Date: 10 FEB 1977 2217-EST
Sender: ELLEN at MIT-MC
From: ELLEN at MIT-MC (V. Ellen Lewis )
To: jmc at SU-AI
Message-ID: <[MIT-MC].34095>

Hello.  I apologise for the delay.  The draft of the LISP Manual which you
have is Parts 1 and 2, which are now available.  Part 3, which considers the
LISP system in general, will (very strong future tense! -- I also work with
Bill Martin so am versed in semantics, syntax, etc! --) be at the printers
by the end of next week, or at worst by the end of February.  A draft copy
of this part can be had if you FTP to SAIL  MC:ELLEN;PART3 DOC  (lineprinter
Pub output...). 
Many thanks for part 3.

∂10-Feb-77  1936	JMC  
To:   ellen at MIT-MC  
Many thanks for part 3.

∂10-Feb-77  1706	JMC  
To:   carl at MIT-AI   
I accept with pleasure.

∂10-Feb-77  1037	JMC  
To:   DSB    
I can give you a copy of a paper I gave at AAAS meeting last year.
There has been much enthusiasm for cable TV in this connection, but
I am not one of the enthusiasts, because (i) the telephone system
is good enough in performance and cost (ii) cable TV is not everywhere
yet, and the rest of the required technology is ready to go (iii)
cable TV is structured as a set of local monopolies whose main
business is in TV, so new services will be dominated by the interests
of the cable TV company.

∂09-Feb-77  1656	JMC  
To:   RWW    
Vera and I accept with pleasure.  It's 7pm, isn't it?

∂09-Feb-77  1137	JMC  
To:   phw at MIT-AI    
I wrote to Meltzer that the paper should be published as revised.

∂09-Feb-77  0526	JMC  	Lisp equations
To:   MDD    
What can be said about solving Lisp equations, e.g.
((x . a) . y) = (y . (b . a)).  They are in some respects
simpler than string equations because of the lack of
associativity, but they may be more important in relation
to pattern recognition.

∂08-Feb-77  0720	JMC  
To:   PAT    
Have you looked for a letter asking about Wise in the incoming?

∂07-Feb-77  1921	JMC  	your proof    
To:   WP
It seems to me to be a metamathematical argument.  Can you give an
argument that involves just substituting a suitable function for
g, as my converse argument involved just making q(x,y) ≡ y = g(x)?

∂07-Feb-77  1407	JMC  	256K core
To:   dbrown at SUMEX-AIM, feigenbaum at SUMEX-AIM   
	As you probably know the rest of our core was installed
last Thursday morning.  It has made a big improvement.  With 30
users, they were getting 22percent before and 62 percent after.
Incidentally, CMU still doesn't have 256K core, which accounts
for their bad experience.  Theirs is overdue.

∂06-Feb-77  0021	JMC  
To:   pratt at MIT-AI  
I'll study CGOL and make some suggestions, but it is unlikely that
a local dialect will arise here, because I have other things to do,
and the MACLISP hackers here, Dick Gabriel and Martin Brooks, don't
use CGOL.  I guess I don't even know how the present Lisp compiler
treats iteration.

∂05-Feb-77  1917	JMC  	reply    
To:   pratt at MIT-AI  
Got your message.  Think we might be able to come close to agreement,
and I'll try to work out a desirable notation, but first I must try out
CGOL some more so as to avoid pointless innovation.

∂05-Feb-77  1832	JMC  	Bureaucracy   
To:   LES    
It seems to me that if an unknown manages to use a large amount of
computer time, bureaucracy conceals who it was, because miscellaneous
is merely totalled.  Any account using over a trivial amount should
be listed in bureaucracy.

∂05-Feb-77  1826	JMC  	Datapoint emulator in Telnet 
To:   JBR    
I observed a random refugee from M.I.T. called ED on his way to
Antarctica using 20 percent of the computer in Telnet.  It seems
he was using a Datapoint Emulation feature in Telnet that Gosper
says Stallman installed on a visit.  Suggest you disable it.

∂05-Feb-77  1741	JMC  
To:   LES    
I missed him, but ED seems to be an M.I.T. hacker far from home.

∂05-Feb-77  1545	JMC  	CGOL.GRU[W77,JMC]  
To:   pratt at MIT-AI  
This file contains the present state of my CGOL grumbles.  As you will
see, I am trying to optimize something different from what you
have been optimizing.  You will also note that I haven't got very far
into CGOL.

∂15-Mar-77  1315	JMC  
To:   nilsson at SRI-KL
Postponing the seminar to the 28th is fine with me.

∂16-Mar-77  0000	JMC  
To:   feigenbaum at SUMEX-AIM    
title: Epistemological Problems of AI.  Paper: McCarthy and Hayes - Some
Philosophical Problems from the Standpoint of Artificial Intelligence -
MI4.  (I may recommend a new paper if it's ready in time, but I won't know
by the first day.)

∂16-Mar-77  0003	JMC  
To:   RCM    
Thanks. It's quite usable.

∂16-Mar-77  0223	JMC  
To:   DCL    
Yes. I called it to the musicians' attention today and will press them
to reduce it.

∂16-Mar-77  1025	JMC  
To:   PAM    
Fine, I'll look today.

∂16-Mar-77  1143	JMC  
To:   DCL    
jed works for Terry and is not a musician so far as we know.

∂16-Mar-77  1236	JMC  
To:   PAM    
I couldn't find the manual on your desk.

∂16-Mar-77  1623	JMC  
To:   PAT    
Please decorate suppes.le1

∂16-Mar-77  2216	JMC  
To:   JC
There are 5 220 jobs logged in now.

∂16-Mar-77  2220	JMC  
To:   JC
The 5 are SEK, KIP, RT, JOS, and BGH.

∂16-Mar-77  2227	JMC  	usage    
To:   SEK, KIP, RT, JOS, BGH
According to our agreement with John Chowning, Music 220 students, with
one exception whose name I forget, are supposed to use the machine between
3am and 9am.  Music 220 was the largest single user group during the first
half of March, the second being other music use.  The two amount to 35%,
of total usage which includes system services,
and this is much more than music's share.  Please use the machine at the
agreed hours.

∂17-Mar-77  1511	JMC  
To:   PAM    
1. I suggest you write one page on how to run MACLISP at LOTS and include
it with the manual you give to Moira tomorrow.  It can be supplemented with
a handout later when we know more.  If 35 is the estimated residual enrollment,
have them make 45.

∂18-Mar-77  0010	JMC  
To:   erman at CMU-10B 
I'll have a definite reaction before your deadline, but my preliminary
reaction is that the two structure don't have the same fringe and
my SAMEFRINGE says so.  The fringes are (A B NIL NIL) and (A NIL B NIL).
The problem refers to S-expressions not lists as I understood it, but
I want to look at how the others understood the problem.

∂18-Mar-77  1436	JMC  
To:   RDR    
There isn't much point in publicity until facilities are actually
available.

∂18-Mar-77  1453	JMC  
To:   RDR    
Yes, I get SCIP bulletin, and I don't share your suspicions.

∂18-Mar-77  1510	JMC  
To:   PAT    
Please print andrei.le8[let,jmc] and include copies of mental, concep,
first, and minima.

∂18-Mar-77  1701	JMC  
To:   MJL    
I would like to teach cs206 in fall and cs226 (representation problem
in AI) in Spring (preferably) or in Winter ( if it fits better).

∂19-Mar-77  0245	JMC  	Cache hits.   
To:   JBR    
The fraction of cache hits might be increased by preferring to schedule
another job running E if the job just run was E.

∂19-Mar-77  1355	JMC  
To:   JBR    
Yes, upper segment cache hits were all I was hoping for.

∂19-Mar-77  2135	JMC  
To:   KRD    
I just received a belated announcement of a conference on AI and
philosophy.  The conference announcement
lists many papers.   There is a rather poor
paper in one of the IJCAI by Aaron Sloman.
I presume you meant my paper with Hayes; my paper with Painter was
on correctness of compilers.  The file mental.xgp[f76,jmc] is such
a paper.  Various philosophers like Nuel Belnap are intersted.

∂20-Mar-77  1216	JMC  
To:   LES    
I agree with all that, and I'll be in this evening.

∂20-Mar-77  1232	JMC  
To:   reddy at CMU-10B 
I would like to accept your invitation to visit Carnegie,
and Monday May 2 would be most convenient, since I want to spend
a week in Europe after the Repino meeting and want to teach my
Tuesday May 3 class.  Is this OK.  I want to plan the Pittsburgh
trip to reduce the costs in time and money of the MI9 trip.

∂20-Mar-77  1234	JMC  
To:   PAT    
Please put the right address on sandew.le1 and pub it.

∂20-Mar-77  1239	JMC  
To:   PAT    
Please put the right address on sandew.le1 and pub it.
Note how the accent on Linkoping is done.
I haven't checked it, so see if it comes out right.

∂22-Mar-77  1101	JMC  
To:   LES    
Please check the numbers in carlst.me1[let,jmc].

∂22-Mar-77  1123	JMC  
To:   carlstrom at USC-ISI
CC:   LES 
Dear Dave:

	We think ARPA is making a serious mistake in cutting so severely
the basic AI research, formal reasoning and mathematical theory of
computation parts of the proposal.  Basic research is the foundation on
which applied research is based.  We hope that our new proposal, which you
haven't seen yet, makes the connection between basic research and defense
applications better than we have in the past.  We tried to present the
basic research in a way that will make it easy for you to expain its
relevance to management.  Please let me know whether the new version is
helpful.  Nevertheless, we despair that ARPA, having already decided to
reduce the effort, will be fully convinced.

	There is, however, hope of getting other support, especially from
NSF for this work, although it will take some time, and it is difficult to
get money for research associates from NSF.  Do you think the following
would be acceptable to ARPA?

	1. We will proceed at the level of effort planned in our original
proposal.

	2. We will charge ARPA for only a fraction of the project's costs.

	3. The ARPA share would be 220K for basic AI and formal reasoning
and 80K for mathematical theory of computation totalling 300K compared to
566K in our original budget and 200K in your revised budget.

	4. If other support is long delayed, we will sharply reduce the
level of effort, but we should have some word from NSF by Fall.

	If ARPA cannot provide the additional 100K (to bring its share to
300K), then we will have to reduce the level of effort in July.

					John McCarthy

∂22-Mar-77  1316	JMC  
To:   JC
CC:   JAM    
$70K plus tax and license?

∂23-Mar-77  1150	JMC  
To:   nilsson at SRI-KL
If I get NSF travel money.

∂24-Mar-77  0025	JMC  
To:   RWW    
Martin Davis will be here today (Thursday).

∂24-Mar-77  0105	JMC  	Correctness of samefringe.   
To:   RWW    
It looks like the following predicate will work for proving the termination
of samefringe: P(u) ≡ ∀x.(fringe x = u ⊃ ∀y.isetv samefringe(x,y)).  The
proof is by ordinary structural induction on u.  If you think it will work,
you might try to push it through.

∂24-Mar-77  0220	JMC  
To:   RWW    
Equivalently P(u) ≡ ∀x y.(fringe x = u ⊃ isetv samefringe(x,y)).

∂25-Mar-77  2106	JMC  
To:   PAM    
 ∂25-Mar-77  1644	PAM  	class notes   
The entire department is shocked; your first 45 pages (and coincidently
45 copies) of class notes are ready. I have been told that the department
will pay for 50 pages of handouts per student, so I need to tell them
how much to charge for the class notes based on how many total
pages you will be handing out. I'll bring you back the original over the weekend.

Paul
Let's call it 110.

∂26-Mar-77  1138	JMC  
To:   gillogly at CMU-10A   
Thanks, I have enough references.

∂26-Mar-77  2300	JMC  
To:   TW
WINOGRAD.FS[W77,JMC] is a draft of my Future Study comments on your paper.

∂27-Mar-77  1359	JMC  
To:   minsky at MIT-AI 
Dear Marvin:

	MINSKY.FS[F76,JMC] is a draft of my comments on your paper for the
Future Study.  Besides that, there are a few rough edges that I suppose
you will want to iron out, so I haven't mentioned them in my direct
comments:

	1. First it seems to me that you forgot the promise in the first
sentence to discuss "the problems and promises that arise from the
prospect of" AI.  Recounting the opinions of science fiction writers seems
inadequate.  You should either discuss it more or change the focus of the
introduction.

	2. Ran out of time.  There is no "second".

				Best Regards,

∂27-Mar-77  2043	JMC  
To:   Dertouzos at MIT-MULTICS   
I have finished all comments.  You'll get them this week.

∂28-Mar-77  1246	JMC  
To:   minsky at MIT-AI 
It is now page 18 of STUDY.FS[W77,JMC].  Sorry.

∂29-Mar-77  1549	JMC  
To:   PAM    
Remind me to tell students charged $2.00 for notes to get $.80 refund.

∂31-Mar-77  1443	JMC  
To:   PHON[ESS,JMC]    
Wegbreit		494-4432

∂31-Mar-77  2218	JMC  
To:   PAM, JAB    
Please react to Gerson for LOTS.

∂01-Apr-77  1103	JMC  
To:   ryland at RUTGERS-10  
1. We are operating with almost no security - either physical or
file - and plan to continue that way unless something bad happens.
The computer is available 24 hours a day without operators at any
time.  At present there is a student guard at the building entrance,
but as soon as partitions have been installed to separate the
computer area from the education area which has no doors on the offices,
we expect to dspense with the guard.

	We use the file security provided by TOPS-20.  Each user has
a password, and he can protect his files or leave them public at his
choice.  We have an accounting system, slightly modified from DEC's,
but since our users - restricted to students and unsponsored research -
are not ccarged, we use it only for monitoring purposes.

	The languages in use include machine language, Fortran (DEC's)
SAIL (an Algol dialect), BLISS (from CMU; it's very expensive in computer
time), LISP (M.I.T.'s Maclisp), BASIC, MIX, PPL, and others.

∂01-Apr-77  2145	JMC  
To:   PAT    
Find except that the return should be open from Stockholm.  I'm staying in
Sweden for a few days.

∂02-Apr-77  1515	JMC  
To:   PAM    
Please phone 321-7580 or 497-4430.

∂04-Apr-77  1030	JMC  
To:   MJL    
How many now for the AI quals?

∂04-Apr-77  1102	JMC  
To:   berliner at CMU-10B   
⊗berlin.me1

∂04-Apr-77  1121	JMC  
To:   ryland at RUTGERS-10  
We will be interested in your experience.  Details about ours can be obtained
from the Manager, Ralph Gorin, who is REG on this machine.
You may be interested in DIALNE[W77,JMC] which gives a plan for ARPANET like
communication using the ordinary telephone system.  If you are interested in
participating in Dialnet, please let me know.

∂04-Apr-77  1211	JMC  	terminal 
To:   JMC    
	Thanks very much for the loan of the TI.  It is a wonderful
gadget.  I must conive to afford one.
					Whit
p.s. It is on your desk.

∂04-Apr-77  1634	JMC  	MTC QUAL 
To:   dbrown at SUMEX-AIM   
Martin Brooks tells me that he has the word that he must take an
MTC qual and that others are also interested.  I am willing, with
the help of Zohar Manna which I shall solicit, to be in charge of one
given in late May.  If this is in accordance with your and Ed's views,
send me a message and ask Moira to announce it and ask for signups.
It will be oral.

∂05-Apr-77  1021	JMC  
To:   berliner at CMU-10B   
Do you think it would be possible to break with the tradition
of analyzing computer chess games as though they were human, i.e. where
you can't look into their heads?  Could you persuade Slate and Atkins
to provide reasonably complete traces of what the machine was thinking
about at the critical points of the game with Levy and combine your
traditional chess player's analysis with your computer scientist's analysis
of where the machine misused its computational resources?
It would be good if Slate and Atkins could be persuaded to rerun
critical decisions, conceivably even with other parameters.  Publishing
such an analysis in the SIGART Newsletter would
increase interest in better chess programs.

This is the message I tried to send yesterday.

∂05-Apr-77  2319	JMC  
To:   RWG    
They are brothers.